stepn(1,step((umc1,alpha_1_), (ci,alpha_1_),tm(s,[ctxm(alpha_1_,umc,ip, (ip,umc1), (ip,umc1)),ctxm(alpha_1_,ci,ip, (ip,ci), (ip,ci))],pri(lst,[pri(hash,[ctxm(alpha_1_,u,bsn,i_bsn,i_bsn)]),ctxm(alpha_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(alpha_1_,u, (d,all,2), (i,d_2), (c,d_2)),ctxm(alpha_1_,u, (d,all,3), (i,d_3), (c,d_3))])))).
stepn(2,step((umc1,alpha_1_), (umc1,alpha_1_),tm(st,pri(lst,[ctxm(alpha_1_,u,bsn,i_bsn,i_bsn),pri(hash,[ctxm(alpha_1_,u,bsn,i_bsn,i_bsn)])])))).
stepn(3,step((ci,alpha_1_), (ci,alpha_1_),tm(st,pri(lst,[pri(hash,[ctxm(alpha_1_,u,bsn,i_bsn,i_bsn)]),ctxm(alpha_1_,umc,ip, (ip,umc1), (ip,umc1)),ctxm(alpha_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(alpha_1_,u, (d,all,2), (i,d_2), (c,d_2)),ctxm(alpha_1_,u, (d,all,3), (i,d_3), (c,d_3))])))).
stepn(4,step((umc2,alpha_2_), (ci,alpha_2_),tm(s,[ctxm(alpha_2_,umc,ip, (ip,umc2), (ip,umc2)),ctxm(alpha_2_,ci,ip, (ip,ci), (ip,ci))],pri(lst,[pri(hash,[ctxm(alpha_2_,u,bsn,i_bsn,i_bsn)]),ctxm(alpha_2_,u, (d,all,1), (i,d_5), (c,d_5)),ctxm(alpha_2_,u, (d,all,2), (i,d_6), (c,d_6)),ctxm(alpha_2_,u, (d,all,3), (i,d_7), (c,d_7))])))).
stepn(5,step((umc2,alpha_2_), (umc2,alpha_2_),tm(st,pri(lst,[ctxm(alpha_2_,u,bsn,i_bsn,i_bsn),pri(hash,[ctxm(alpha_2_,u,bsn,i_bsn,i_bsn)])])))).
stepn(6,step((ci,alpha_2_), (ci,alpha_2_),tm(st,pri(lst,[pri(hash,[ctxm(alpha_2_,u,bsn,i_bsn,i_bsn)]),ctxm(alpha_2_,umc,ip, (ip,umc2), (ip,umc2)),ctxm(alpha_2_,u, (d,all,1), (i,d_5), (c,d_5)),ctxm(alpha_2_,u, (d,all,2), (i,d_6), (c,d_6)),ctxm(alpha_2_,u, (d,all,3), (i,d_7), (c,d_7))])))).
stepn(7,step((ci,beta_1_), (r,beta_1_),tm(s,[ctxm(beta_1_,ci,ip, (ip,ci), (ip,ci)),ctxm(beta_1_,r,ip, (ip,r), (ip,r))],pri(lst,[pri(hash,[pri(lst,[pri(hash,[ctxm(beta_1_,u,bsn,i_bsn,i_bsn)]),ctxm(beta_1_,r,dom, (dom,r,beta_1_), (dom,r,beta_1_))])]),ctxm(beta_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(beta_1_,u, (d,all,2), (i,d_5), (c,d_5))])))).
stepn(8,step((ci,beta_1_), (ci,beta_1_),tm(st,pri(lst,[pri(hash,[ctxm(beta_1_,u,bsn,i_bsn,i_bsn)]),pri(hash,[pri(lst,[pri(hash,[ctxm(beta_1_,u,bsn,i_bsn,i_bsn)]),ctxm(beta_1_,r,dom, (dom,r,beta_1_), (dom,r,beta_1_))])]),ctxm(beta_1_,r,dom, (dom,r,beta_1_), (dom,r,beta_1_)),ctxm(beta_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(beta_1_,u, (d,all,2), (i,d_5), (c,d_5))])))).
stepn(9,step((r,beta_1_), (r,beta_1_),tm(st,pri(lst,[pri(hash,[pri(lst,[pri(hash,[ctxm(beta_1_,u,bsn,i_bsn,i_bsn)]),ctxm(beta_1_,r,dom, (dom,r,beta_1_), (dom,r,beta_1_))])]),ctxm(beta_1_,r,ip, (ip,r), (ip,r)),ctxm(beta_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(beta_1_,u, (d,all,2), (i,d_5), (c,d_5))])))).
stepn(10,step((ci,beta_2_), (r,beta_2_),tm(s,[ctxm(beta_2_,ci,ip, (ip,ci), (ip,ci)),ctxm(beta_2_,r,ip, (ip,r), (ip,r))],pri(lst,[pri(hash,[pri(lst,[pri(hash,[ctxm(beta_2_,u,bsn,i_bsn,i_bsn)]),ctxm(beta_2_,r,dom, (dom,r,beta_2_), (dom,r,beta_2_))])]),ctxm(beta_2_,u, (d,all,1), (i,d_2), (c,d_2)),ctxm(beta_2_,u, (d,all,2), (i,d_6), (c,d_6))])))).
stepn(11,step((ci,beta_2_), (ci,beta_2_),tm(st,pri(lst,[pri(hash,[ctxm(beta_2_,u,bsn,i_bsn,i_bsn)]),pri(hash,[pri(lst,[pri(hash,[ctxm(beta_2_,u,bsn,i_bsn,i_bsn)]),ctxm(beta_2_,r,dom, (dom,r,beta_2_), (dom,r,beta_2_))])]),ctxm(beta_2_,r,dom, (dom,r,beta_2_), (dom,r,beta_2_)),ctxm(beta_2_,u, (d,all,1), (i,d_2), (c,d_2)),ctxm(beta_2_,u, (d,all,2), (i,d_6), (c,d_6))])))).
stepn(12,step((r,beta_2_), (r,beta_2_),tm(st,pri(lst,[pri(hash,[pri(lst,[pri(hash,[ctxm(beta_2_,u,bsn,i_bsn,i_bsn)]),ctxm(beta_2_,r,dom, (dom,r,beta_2_), (dom,r,beta_2_))])]),ctxm(beta_2_,r,ip, (ip,r), (ip,r)),ctxm(beta_2_,u, (d,all,1), (i,d_2), (c,d_2)),ctxm(beta_2_,u, (d,all,2), (i,d_6), (c,d_6))])))).
